| Definitions | s = t, t  T, ES, AbsInterface(A), E(X), x:A  B(x), e c e',  x:A. B(x), P   Q,  A, x:A  B(x),  b, left + right, P  Q, (e < e'), {x:A| B(x)} , Void, False, Top, f(a), prior-f-fixedpoints(e), (x l), E,  , type List, f**(e), a:A fp B(a), Type, EqDecider(T), Unit, IdLnk, Id, EOrderAxioms(E; pred?; info), EState(T), Knd,   x. t(x), x,y. t(x;y), kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M),  ,  , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r s, constant_function(f;A;B), P & Q, strong-subtype(A;B), loc(e), kind(e), let x,y = A in B(x;y),  , S  T,  , Outcome, #$n, A B, a < b, ||as||, l[i], |g|, A c B, e loc e' , (e <loc e'), X(e), e(e1,e2].P(e), @e(x v), (last change to x before e), pred(e),  x:A. B(x), P  Q, P Q, lastchange(x;e), es-init(es;e), True, sender(e), [], <a, b>, prior(X), e  X, A List , [car / cdr], loc(e), case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , as @ bs, ff, b, tt, p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, x f y, a < b, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), a = b, a = b, deq-member(eq;x;L), e = e', p q, p q, p q, {T}, n+m, n - m, SWellFounded(R(x;y)), pred!(e;e'),  x:A.B(x), suptype(S; T), first(e), pred(e), x.A(x), i  j , -n, f g, f(x)?z, vartype(i;x), state@i, State(ds), State(ds), x dom(f),  T, t ...$L |
| Lemmas | es-fix-equal, es-fix-causle, es-causle transitivity, es-fix wf, member singleton, es-causle weakening locl, es-le weakening eq, es-causl weakening, es-causl transitivity1, es-causle weakening, true wf, squash wf, subtype rel function, subtype rel sum, es-prior-interface-locl, member append, ge wf, nat properties, es-interface wf, kind wf, loc wf, first wf, pred! wf, strongwellfounded wf, es-causl-swellfnd, nat ind tp, guard wf, le wf, not functionality wrt iff, assert-es-eq-E-2, es-eq-E wf, false wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, es-is-interface wf, bnot wf, not wf, append wf, es-interface-val wf2, es-prior-interface wf, es-interface-val wf, es-le-causle, es-causle-le, es-causl wf, es-locl wf, es-le wf, es-causle wf, length wf1, select wf, l member wf, es-prior-fixedpoints wf, es-fix wf2, es-E-interface wf, es-E wf, member wf, top wf, constant function wf, assert wf, bool wf, qle wf, cless wf, val-axiom wf, rationals wf, nat wf, Msg wf, kindcase wf, Knd wf, EState wf, EOrderAxioms wf, Id wf, IdLnk wf, unit wf, deq wf, event system wf, subtype rel wf, es-E-interface-subtype rel |